minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
↳ QTRS
↳ Overlay + Local Confluence
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
GE(s(x), s(y)) → GE(x, y)
GT(s(x), s(y)) → GT(x, y)
DIV(x, y) → IF1(ge(x, y), x, y)
DIV(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF2(true, x, y) → DIV(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
GE(s(x), s(y)) → GE(x, y)
GT(s(x), s(y)) → GT(x, y)
DIV(x, y) → IF1(ge(x, y), x, y)
DIV(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF2(true, x, y) → DIV(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
DIV(0, s(x0)) → IF1(false, 0, s(x0))
DIV(x0, 0) → IF1(true, x0, 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
IF2(true, x, y) → DIV(minus(x, y), y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
DIV(0, s(x0)) → IF1(false, 0, s(x0))
DIV(x0, 0) → IF1(true, x0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x0, 0) → IF1(true, x0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x0, 0) → IF1(true, x0, 0)
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF2(true, s(x0), x1) → DIV(if(gt(s(x0), x1), x0, x1), x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF2(true, s(x0), x1) → DIV(if(gt(s(x0), x1), x0, x1), x1)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF2(true, s(x0), x1) → DIV(if(gt(s(x0), x1), x0, x1), x1)
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF2(true, s(z0), s(z1)) → DIV(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → DIV(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF2(true, s(z0), s(z1)) → DIV(if(gt(z0, z1), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → DIV(if(gt(z0, z1), z0, s(z1)), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(IF1(x1, x2, x3)) = x2
POL(IF2(x1, x2, x3)) = x2
POL(false) = 0
POL(ge(x1, x2)) = 1 + x2
POL(gt(x1, x2)) = x1
POL(if(x1, x2, x3)) = 1 + x2
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QTRS
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a40](witness_sort[a40], witness_sort[a40]) → true
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a40](witness_sort[a40], witness_sort[a40]) → true
[true, false, 0, minus2, if3, equalsort[a23]2, equalsort[a40]2] > s1 > [minus'2, if'3] > gt2
ge2 > gt2
equalbool2 > gt2
and2 > gt2
or2 > gt2
isatrue1 > gt2
isafalse1 > gt2
witnesssort[a40] > gt2
equalsort[a23]2: multiset
equalsort[a40]2: [1,2]
minus2: [2,1]
minus'2: [2,1]
true: multiset
or2: multiset
and2: multiset
gt2: multiset
0: multiset
equalbool2: multiset
if3: [3,2,1]
if'3: [3,2,1]
isafalse1: multiset
witnesssort[a40]: multiset
false: multiset
s1: multiset
ge2: [1,2]
isatrue1: multiset
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a40](witness_sort[a40], witness_sort[a40]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRSRRRProof
not(false) → true
not(true) → false
not(false) → true
not(true) → false
[not1, false] > true
not1: [1]
true: multiset
false: multiset
not(false) → true
not(true) → false
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof
↳ QTRSRRRProof
not(false) → true
not(true) → false
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(false) = 0
POL(not(x1)) = 1 + x1
POL(true) = 0
not(false) → true
not(true) → false
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRSRRRProof
↳ QTRS